%Show scalability table/figure describing how the execution time changes
%with/out pruning, and with different sizes of the search space. In each of
% those cases, we can also plot/show the numbers to demonstrate how the size of the
%formula in USE changes and how does that affect the execution time.
%
%Discuss the results. How the search space increases with an increase in the
%number of classes. Show for example, if we remove a rule, how will this affect
%the runtime, the size of the formula, etc.
To explore the performance of our approach, we used the verification prototype
to verify the 18 constraints (Table~\ref{tab:OCLConsts}) for different
scopes. We ran the verification with scopes between one and 12. We only show the
results for scopes 6, 8, 10, and 12 due to the page limit. The scope determines
the maximum number of objects per concrete class in the search space. In our
tests, we used the same scope for all classes, although it could be set
individually. \begin{changebar}Since our transformation model has 1586 classes, a scope of $n$
generates a model with $1586n$ potential elements (and their corresponding links
and attribute values).\end{changebar} All experiments where run on a standard laptop at 2.50
GHz and 16 GB of memory, using Java 7, Kodkod 2.0, and Glucose 2.1.

For each combination of constraint and scope, the prototype generates
two time values:
the time the prototype takes to translate the relational logic
formula into a propositional formula (i.e., \emph{translation time}) and the
time the SAT solver takes to solve the formula (i.e., \emph{constraint solving
time}).

We show these two time values (in seconds) in Table~\ref{tab:scalres}.
Each column represents the time intervals for each of the 18 constraints, where
the \emph{Constraint Abbreviation} is the abbreviation given to each constraint
in Table~\ref{tab:OCLConsts} (e.g., (M1) and (U5)). Each row represents the time
intervals for a different scope. Thus, each cell within the table shows the
translation time and the constraint solving time of a certain constraint at a
specific scope.
% \begin{figure*}[tbh]
%  \resizebox{1\textwidth}{!}{%
%   \includegraphics{imgs/completeScalRes.jpg}
%  }
% \caption{Scalability results for the 18 constraints on different search space
% sizes}
% \label{fig:scalres}
% \vspace{-0.6cm}
% \end{figure*}
%%%%
% \begin{table}[tbh]%tbh !h
%  	\centering
%  	\scriptsize
% \begin{tabular}{c}
%  {\resizebox{1\textwidth}{!}{\includegraphics{imgs/scalRes_part1.jpg}}}
%  \end{tabular}
% \caption{Scalabaility results for the Multiplicity Invariants, Security
% Invariants, and Pattern Contracts.}
% \label{tab:scalres_P1}
% \end{table}
% \begin{table}[tbh]%tbh !h
%  	\centering
%  	\scriptsize
% \begin{tabular}{c}
%  {\resizebox{1\textwidth}{!}{\includegraphics{imgs/scalRes_part2.jpg}}}
%  \end{tabular}
% \caption{Scalabaility results for the Uniqueness Contracts.}
% \label{tab:scalres_P2}
% \end{table}
%%%%
% \begin{table}[!h]%tbh !h
%  	\centering
%  	\scriptsize
% \begin{tabular}{c}
%  {\resizebox{1\textwidth}{!}{\includegraphics{imgs/completeScalRes.jpg}}}
%  \end{tabular}
% \caption{Scalability results for the 18 constraints on different search space sizes.}
% \label{tab:scalres}
% \end{table}

\begin{table}[tbh]%tbh !h
\vspace*{-0.2cm}
  \centering
  \hspace*{-.6cm}\includegraphics[width=1.1\textwidth]{imgs/NumbersSmall.pdf}\\[-2ex]
  \caption{Translation\textbackslash Constraint Solving times (seconds) for the
18 constraints on different scopes. For a scope of 12, the
 verification of S1 did not terminate in a week.}
\vspace*{-0.5cm}
\label{tab:scalres}
%\vspace{-1cm}
\end{table}
Two observations can be made from Table~\ref{tab:scalres}. First, despite the
exponential complexity of checking boolean satisfiability, we could verify the
postconditions for scopes up to 12 in most of the cases; only the analysis
of S1 did not finish for scope 12; the constraint solving time of S1 in scope 10 was
the longest (just over an hour). Although we have no proof that no bugs will
appear for bigger scopes, we are confident that a scope of 12 was sufficient to
uncover any bugs in our transformation with respect to the defined constraints.
In fact, the two bugs that were uncovered and fixed were found at a scope of
one.
% The maximum scope sufficient to show bugs in a transformation is transformation-dependent.
% For example, a transformation with a multiplicity invariant that requires a
% multiplicity to be 10, will require a scope of 11 to generate
% a counterexample for that invariant, if any. We do not have similar constraints
% in our transformation and thus, we are confident that a scope of 5 is sufficient
% to uncover any bugs. To assess the performance of the used approach, we experiment
% with scopes ranging from 4 to 12.

Second, the translation times are larger than expected and grow mostly
polynomially.
% for scope 12,
% translating P1 took almost 6 hours.
This can be attributed to the approach used by Kodkod to unfold a first-order
relational formula into a set of clauses in conjunctive normal form (CNF), given
an upper bound for the relation extents~\cite{Torlak2007Kodkod}.  
%While the translation into CNF is exponential to the length of the formula in
%general, the size of the scopes is dominating.
While transforming a formula into CNF grows exponentially with the length of the
formula, it only grows polynomially with the scope in our case (as the formula's
length does not change significantly). For example, each pair of nested
quantifiers will generate a number of clauses that grows quadratically with the scope. The relational logic
constraints generated implicitly by USE for all associations expand similarly.
This justifies why the two pattern contracts (i.e., P1 and P2) show the highest
translation times; they have the most quantifiers of the 18 constraints.

Using an incremental SAT solver would improve the performance of the prototype.
Since most of the generated Boolean formula is the same for all the 18
constraints (i.e., the encoding of classes, associations, multiplicities, and
preconditions), we expect that the translation (i.e., the first number in each
cell of Table~\ref{tab:scalres}) can be done once for the entire verification
process; except for $P1$ and $P2$ which differ in their high number of nested
quantifiers.
% 
% Notice that we did not use an incremental SAT solver.  Since the specification
% that we verify is mostly unchanged between the verification runs for two
% postconditions, all the relational logic formulas (and hence the CNF clauses)
% encoding the classes, associations, multiplicities, and OCL preconditions stay
% the same. We except that a significant amount of the translation time can be
% pulled up-front (done only one for the whole verification process) using an
% incremental SAT solver. Exception are complex constraints such as P1 and P2, for
% which the translation time is dominated by their high number of nested
% quantifiers. For those postconditions, a significant specific translation time
% would remain.
%
% Kodkod unfolds a first-order
% relational formula by replacing all quatifiers with a conjuction of all possible
% clauses of the quantified variables. The unfolded formula is then transformed
% into a propositional formula in conjunctive normal form (CNF). For example,
% consider the following first-order formula:
% % $\mathtt{forAll(r1:R\mid forAll(r2: R \mid (r1.a=r2.a) implies (r1=r2)))}$ 
% $\mathtt{R.allInstances()\to forAll(r1 : R\mid R.allInstances()\to}$ \\ $\mathtt{forAll(r2 :
% R\mid(r1.a = r2.a) implies (r1=r2)))}$ with the scope of R set to
% 5. In that case, the relational formula is transformed into a propositional
% formula in CNF with 4498012 clauses.  
% Thus, the number of clauses and the
% translation times increases non-linearly with the scope. This justifies why the
% two pattern contracts (i.e., P1 and P2) show the highest translation times; they
% have the most quantifiers of the 18 constraints.
% The constraint solving times exponentially increases with scope, as expected.
% Since the used native SAT solvers are heuristic-based, we claim that
% sophisticated heuristics (e.g. symmetry breaking, lemma learning) are used
% which result in small constraint solving times for small scopes. To confirm
% our claim, further investigation of the SAT solver is needed which is outside
% the scope of this study. The exponential growth of the constraint solving time
% causes it to eventually dominate the translation time.
% Second, we compare between the change in the translation time and constraint
% solving time (i.e., positive or negative change). The translation time always
% increases with an increase in the scope due to the abovementioned reason
% of how quantifiers are unfolded. On the other hand, the constraint solving time
% sometimes decreases with an increase in the scope (e.g. the
% constraint solving time for U2 is smaller at a scope of 6 than it is
% for a scope of 5). This can generally occur with SAT solvers since
% they mostly rely on heuristic based approaches to solve formulae.
% Based on the above two observations and on Table~\ref{tab:scalres}, we make
% several conclusions. First, the two pattern contracts (i.e. P1 and P2) show the
% highest translation times since they have the highest number of quantifiers of
% the 18 constraints. Thus, the constraint solving time of the two pattern
% contracts dominates their translation times only at larger scopes.
% Second, at a scope of 12, constraint xx took the maximum translation time
% (xx sec) and constraint yy took the maximum constraint
% solving time (yy sec). Since the former two numbers represent
% the worst translation and constraint solving times for a scope of 12, we
% claim that the approach scales for acceptable scopes and
% for industrial transformation problems. 
%At a scope of 7, constraint U9 took the maximum translation time
% (120559 ms, i.e. 120.559 sec) and constraint U6 took the maximum constraint
% solving time (51576 ms, i.e. 51.576 sec). Since the former two numbers represent
% the worst translation and constraint solving times for a scope of 7, we
% are confident that the approach scales for acceptable scopes, and
% for large, industrial transformation problems.
% \begin{table}[!h]%tbh
%  	\centering
%  	\footnotesize
%  	\renewcommand{\arraystretch}{2.4}
% \begin{tabular}{|l|l|l|l|}
%  \hline 
%  \parbox{0.16\textwidth}{\it{\bf AB}} & \parbox{0.24\textwidth}{\it{\bf BC}} &
%  \parbox{0.24\textwidth}{\it{\bf CD}} & \parbox{0.24\textwidth}{\it{\bf DE}}\\ \hline
%  {\multirow{5}{2cm}{T}} &
%  \parbox{0.24\textwidth}{T} & \parbox{0.24\textwidth}{A} &
%  \parbox{0.24\textwidth}{r} \\ \cline{2-4}
%   & \parbox{0.24\textwidth}{h} &
%   \parbox{0.24\textwidth}{A} & \parbox{0.24\textwidth}{s} \\ \hline 
%   {\multirow{1}{2cm}{T}} & 
%   \parbox{0.24\textwidth}{y} & \parbox{0.24\textwidth}{x} &
%   \parbox{0.24\textwidth}{x} \\ \cline{2-4}
%   \hline
%  \end{tabular}
% \caption{Scalability test results for the 18 constraints}
% \label{tab:scalabilityTable}
% \end{table}